8.5 KB · ⇊ 3 parts · ⤓ Micron 8.5 KB · ⤓ HTML 71.5 KB

top

Die Computation Tree Logic (kurz CTL) ist eine temporale Logik, deren Modell der Zeit eine baumartige Struktur hat. Die zeitliche Änderung von Zuständen und deren Eigenschaften wird durch Pfade innerhalb dieser Baumstruktur modelliert. Hierbei hat die Zukunft mehrere Pfade, wobei nicht festgelegt ist, welche letztendlich realisiert werden. Demnach können Aussagen über die mögliche Entwicklungen getroffen werden.

Die CTL wird zur Verifikation von Hard- und Software verwendet, üblicherweise von Model Checkern.

Zu der Familie der temporalen Logiken gehört auch die linear temporale Logik (LTL), wobei hier nur eine Zukunft möglich ist. Eine Verallgemeinerung der beiden Logiken wird als CTL* bezeichnet.

• Syntax

• Minimale Grammatik

• Temporale Operatoren

• Semantik

• Literatur

Sei A P {\displaystyle AP} eine Menge von atomaren Aussagen (Behauptungen), dann ist jedes Element p ∈ ∈ A P {\displaystyle p\in AP} eine CTL-Formel. Sind ϕ ϕ {\displaystyle \phi } und ψ ψ {\displaystyle \psi } Formeln, dann auch ¬ ¬ ϕ ϕ {\displaystyle \neg \phi } , ϕ ϕ ∨ ∨ ψ ψ {\displaystyle \phi \lor \psi } , EX ϕ ϕ {\displaystyle {\text{EX}}\phi } , EG ϕ ϕ {\displaystyle {\text{EG}}\phi } und ϕ ϕ EU ψ ψ {\displaystyle \phi {\text{EU}}\psi } . Dies definiert die minimale Grammatik von CTL. In der Regel wird diese allerdings um die gängigen booleschen Operatoren ∧ ∧ {\displaystyle \land } , ⟹ ⟹ {\displaystyle \implies } und ⇔ ⇔ {\displaystyle \Leftrightarrow } , sowie einigen weiteren temporalen Operatoren erweitert.

Die Erweiterung der minimalen Grammatik um folgende Operatoren erhöht nicht die Mächtigkeit der Sprache, da alle Operatoren durch Umformungen zurückgeführt werden können.

• Pfadoperatoren:

• A ϕ ϕ {\displaystyle A\phi } – auf allen Pfaden folgt ϕ ϕ {\displaystyle \phi } (englisch: All)

• E ϕ ϕ {\displaystyle E\phi } – auf mindestens einem Pfad folgt ϕ ϕ {\displaystyle \phi } (englisch: Exists)

• Pfad-spezifische Operatoren:

• X ϕ ϕ {\displaystyle X\phi } – unmittelbar folgt ϕ ϕ {\displaystyle \phi } (englisch: neXt state)

• F ϕ ϕ {\displaystyle F\phi } – irgendwann folgt ϕ ϕ {\displaystyle \phi } (englisch: some Future state oder Finally)

• G ϕ ϕ {\displaystyle G\phi } – auf dem folgenden Pfad folgt in jedem Zustand ϕ ϕ {\displaystyle \phi } (englisch: Globally)

• ϕ ϕ U ψ ψ {\displaystyle \phi U\psi } – ϕ ϕ {\displaystyle \phi } folgt bis zum Erreichen des Zustands ψ ψ {\displaystyle \psi } (englisch: Until)

• ϕ ϕ W ψ ψ {\displaystyle \phi W\psi } – ϕ ϕ {\displaystyle \phi } folgt immer oder bis zum Erreichen des Zustands ψ ψ {\displaystyle \psi } (englisch: Weak Until)

Pfad und pfad-spezifische Operatoren können miteinander kombiniert werden, sodass sich beispielsweise folgende Formeln ergeben:

• E X ϕ ϕ {\displaystyle EX\phi } – in (mind.) einem nächsten Zustand gilt ϕ ϕ {\displaystyle \phi }

• E F ϕ ϕ {\displaystyle EF\phi } – in (mind.) einem der folgenden Zustände gilt ϕ ϕ {\displaystyle \phi }

• E G ϕ ϕ {\displaystyle EG\phi } – es gibt (mind.) einen Pfad, so dass ϕ ϕ {\displaystyle \phi } entlang des ganzen Pfades gilt

• E [ ϕ ϕ U ψ ψ ] {\displaystyle E[\phi U\psi ]} – es gibt einen Pfad, für den gilt: bis zum ersten Auftreten von ψ ψ {\displaystyle \psi } gilt ϕ ϕ {\displaystyle \phi }

• A X ϕ ϕ {\displaystyle AX\phi } – in jedem nächsten Zustand gilt ϕ ϕ {\displaystyle \phi }

• A F ϕ ϕ {\displaystyle AF\phi } – man erreicht immer einen Zustand, in dem ϕ ϕ {\displaystyle \phi } gilt

• A G ϕ ϕ {\displaystyle AG\phi } – auf allen Pfaden gilt in jedem Zustand ϕ ϕ {\displaystyle \phi }

• A [ ϕ ϕ U ψ ψ ] {\displaystyle A[\phi U\psi ]} – es gilt immer ϕ ϕ {\displaystyle \phi } bis zum ersten Auftreten von ψ ψ {\displaystyle \psi }

CTL Formeln werden über Transitionssysteme definiert. Für eine gegebene Folge von Zuständen des Systems T ( s 0 ) = s 0 , s 1 , … … {\displaystyle T(s_{0})=s_{0},s_{1},\ldots } (beginnend in Zustand s 0 {\displaystyle s_{0}} ) sind die Operatoren formal wie folgt definiert, dabei steht T ( s 0 ) ⊨ ⊨ ϕ ϕ {\displaystyle T(s_{0})\models \phi } für T ( s 0 ) {\displaystyle T(s_{0})} erfüllt ϕ ϕ {\displaystyle \phi } :

• T ( s 0 ) ⊨ ⊨ ¬ ¬ ϕ ϕ ⇔ ⇔ T ( s 0 ) ⊭ ϕ ϕ {\displaystyle T(s_{0})\models \neg \phi \quad \Leftrightarrow \quad T(s_{0})\not \models \phi }

• T ( s 0 ) ⊨ ⊨ ϕ ϕ ∨ ∨ ψ ψ ⇔ ⇔ T ( s 0 ) ⊨ ⊨ ϕ ϕ oder T ( s 0 ) ⊨ ⊨ ψ ψ {\displaystyle T(s_{0})\models \phi \lor \psi \quad \Leftrightarrow \quad T(s_{0})\models \phi {\text{ oder }}T(s_{0})\models \psi }

• T ( s 0 ) ⊨ ⊨ E X ϕ ϕ ⇔ ⇔ T ( s 1 ) ⊨ ⊨ ϕ ϕ {\displaystyle T(s_{0})\models EX\phi \quad \Leftrightarrow \quad T(s_{1})\models \phi }

• T ( s 0 ) ⊨ ⊨ E G ϕ ϕ ⇔ ⇔ ∀ ∀ i : T ( s i ) ⊨ ⊨ ϕ ϕ {\displaystyle T(s_{0})\models EG\phi \quad \Leftrightarrow \quad \forall i:T(s_{i})\models \phi }

• T ( s 0 ) ⊨ ⊨ ϕ ϕ E U ψ ψ ⇔ ⇔ ∃ ∃ k : T ( s k ) ⊨ ⊨ ψ ψ ∧ ∧ ∀ ∀ i < k : T ( s i ) ⊨ ⊨ ϕ ϕ {\displaystyle T(s_{0})\models \phi EU\psi \quad \Leftrightarrow \quad \exists k:T(s_{k})\models \psi \land \forall i<k:T(s_{i})\models \phi }

Die oben genannten Umformungen erlauben es, Formeln ineinander umzuwandeln.

• ¬ ¬ A ϕ ϕ ≡ ≡ E ¬ ¬ ϕ ϕ {\displaystyle \neg A\phi \equiv E\neg \phi }

• ¬ ¬ A F ϕ ϕ ≡ ≡ E G ¬ ¬ ϕ ϕ {\displaystyle \neg AF\phi \equiv EG\neg \phi }

• ¬ ¬ E F ϕ ϕ ≡ ≡ A G ¬ ¬ ϕ ϕ {\displaystyle \neg EF\phi \equiv AG\neg \phi }

• ¬ ¬ A X ϕ ϕ ≡ ≡ E X ¬ ¬ ϕ ϕ {\displaystyle \neg AX\phi \equiv EX\neg \phi }

• A G ϕ ϕ ≡ ≡ ϕ ϕ ∧ ∧ A X A G ϕ ϕ {\displaystyle AG\phi \equiv \phi \land AXAG\phi }

• E G ϕ ϕ ≡ ≡ ϕ ϕ ∧ ∧ E X E G ϕ ϕ {\displaystyle EG\phi \equiv \phi \land EXEG\phi }

• A F ϕ ϕ ≡ ≡ ϕ ϕ ∨ ∨ A X A F ϕ ϕ {\displaystyle AF\phi \equiv \phi \lor AXAF\phi }

• E F ϕ ϕ ≡ ≡ ϕ ϕ ∨ ∨ E X E F ϕ ϕ {\displaystyle EF\phi \equiv \phi \lor EXEF\phi }

• A [ ϕ ϕ U ψ ψ ] ≡ ≡ ψ ψ ∨ ∨ ( ϕ ϕ ∧ ∧ A X A [ ϕ ϕ U ψ ψ ] ) {\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}

• E [ ϕ ϕ U ψ ψ ] ≡ ≡ ψ ψ ∨ ∨ ( ϕ ϕ ∧ ∧ E X E [ ϕ ϕ U ψ ψ ] ) {\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}

• Clarke, Grumberg, Peled: Model Checking. MIT Press, 2000, ISBN 0-262-03270-8

• Rohit Kapur: CTL for Test Information of Digital ICS. Springer, 2002, ISBN 978-1-4020-7293-2

• B. Berard, Michel Bidoit, Alain Finkel: Systems and Software Verification. Model-checking Techniques and Tools. Springer, 2001, ISBN 3-540-41523-8

• M. Huth and M. Ryan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge, 2004, ISBN 0-521-54310-X